module ctrl;

	// Define the clock
	//
	// 0in set_clock clk -period 10 -waveform { 0 5 } -posedge -default
	
	// Define the reset
	//
	// 0in default_reset rst -async
	
	// Constrain reset to be 0 (inactive) for formal analysis
	//
	// 0in set_constraint rst 1'b0
	
	// Constrain the key
	//
	// 0in set_constraint short_key 2'b01
	
	// Constrain the formal analysis
	//
	// 0in range -var short_plaintext -min 0 -max 3 -assume -module wrapper
	

endmodule